Definitions | t.2, t.1, grp_op(g), grp_car(g), comm(T; op), inverse(T; op; id; inv), ident(T; op; id), assoc(T; op), P Q, x. t(x), P Q, prop{i:l}, P Q, x f y, P Q, x:A. B(x), eqfun_p(T; eq), qadd_grp, abgrp{i:l}, t T, x(s), mon{i:l}, grp{i:l}, subtype(S; T) |